feat: even more general ring switch by alexanderlhicks · Pull Request #615 · Verified-zkEVM/ArkLib

alexanderlhicks · 2026-07-07T15:37:46Z

Further generalization of the ring-switching abstraction based on discussion around https://github.com/leanEthereum/leanVM-b/blob/main/misc/ring-switching-generalized.pdf and Flock.
WIP, but should not be a huge PR once the generic layer (mostly in the current draft) is in place, binius and hachi (if the ring switching stage is reached before this is merged) will be ported accordingly.

github-actions · 2026-07-07T15:41:46Z

🤖 PR Summary

This PR generalizes the ring-switching layer to decoupled packing and opening algebras, as documented in Flock (BRW26) and the internal note RSG. The core change is the introduction of the Generic ring-switching subdirectory (ArkLib/ProofSystem/RingSwitching/Generic/) with five new files that define and prove the foundational structures, packing correctness, batching separation, recombination injectivity, a fixed relation chain, and a PCS binding interface. Supporting infrastructure is added under ArkLib/Data/ (module basis lemmas, MvPolynomial degree bounds, probability oracle compiler bridge) and ArkLib/OracleReduction/ (challenge round factoring). A bug fix in the Binius FRI CoreInteractionPhase replaces a silent diagonal evaluation with the corrected witnessNovelCoeffs. The PR is structurally complete with all new files carrying no sorry or admit.

Statistics

Metric	Count
📝 Files Changed	19
✅ Lines Added	2342
❌ Lines Removed	12

Lean Declarations

✏️ Added: 110 declaration(s)

ArkLib/Data/Module/Basis.lean (2)

theorem sum_smul_bijective (b : Basis ι R M) :
theorem sum_smul_injective (b : Basis ι R M) :

ArkLib/Data/MvPolynomial/Degrees.lean (1)

theorem totalDegree_le_card_of_degreeOf_le_one [Fintype σ] (p : MvPolynomial σ R)

ArkLib/Data/MvPolynomial/Multilinear.lean (4)

theorem MLE_eval_eq_sum_eqTilde (evals : (σ → Fin 2) → R) (r : σ → R) :
theorem MLE_totalDegree_le (evals : (σ → Fin 2) → R) :
theorem aeval_multilinear_eq_sum_eqTilde {A : Type*} [CommRing A] [Algebra R A] [IsDomain A]
theorem coe_boolFun_eq_ite [AddMonoidWithOne R] (u : σ → Fin 2) :

ArkLib/Data/Probability/Instances.lean (1)

lemma prob_schwartz_zippel_single_variable {R : Type} [CommRing R] [IsDomain R] [Fintype R]

ArkLib/Data/Probability/OracleCompBridge.lean (2)

theorem probEvent_bind_uniformSample_le {A : Type} (ma : ProbComp A)
theorem probEvent_uniformSample_eq_pr_uniformOfFintype (E : C → Prop) :

ArkLib/OracleReduction/Security/ChallengeRound.lean (2)

theorem probEvent_challengeRound_le
theorem probEvent_rbrGame_le

ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean (2)

def witnessNovelCoeffs (t : L⦃≤ 1⦄[X Fin ℓ]) : Fin (2^ℓ) → L
example :

ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean (2)

def biniusCommitsTo
lemma initialCompatibility_eq_biniusCommitsTo :

ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean (14)

def decoupledFieldCarrier : RingSwitchCarrier (ZMod 2) where
def eqFold (κ : ℕ) : BatchingStrategy P (Fin κ → Fin 2) where
def gammaPowers (e : ℕ) : BatchingStrategy P (Fin e) where
def reindex {P : Type} [CommRing P] {W : Type} [Fintype W] (bat : BatchingStrategy P W)
example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (e : ℕ) :
example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (κ : ℕ) :
example : BatchingStrategy (ZMod 3) (Fin (2 ^ 2))
example : BatchingStrategy (ZMod 3) (Fin 3)
example : Type 1
example : decoupledFieldCarrier.P = GaloisField 2 2
example :
example :
example :
example :

ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean (15)

def Bmult {m : ℕ} (r : Fin m → car.E) (weight : car.ιE → car.P) : MultilinearPoly car.P m
def boolToE {m : ℕ} (y : Fin m → Fin 2) : Fin m → car.E
def bridge (weight : car.ιE → car.P) : car.E →ₗ[B] car.P
def decoupledToyCarrier : RingSwitchCarrier (ZMod 2) where
def eqCoord {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2) (u : car.ιE) : B
def packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) : MultilinearPoly car.P m
def towerCarrier {K L : Type} [Field K] [Field L] [Algebra K L]
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2) (u : decoupledToyCarrier.ιE) :
example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2)
example (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example : RingSwitchCarrier (ZMod 2)
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
theorem bridge_eqTilde {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2)

ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean (14)

def curryFamily {κ ℓ ℓ' : ℕ} {K : Type} [CommRing K] (h_l : ℓ = ℓ' + κ)
def unpack {m : ℕ} (t' : MultilinearPoly car.P m) : car.ιP → MultilinearPoly B m
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) (pt : Fin 3 → ZMod 2) :
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
example (t' : MultilinearPoly decoupledToyCarrier.P 3) :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) (m : ℕ) :
theorem packMLE_eq_packedMLE_curry {κ : ℕ} [NeZero κ] {K L : Type} [Field K] [Field L] [Algebra K L]
theorem packedMLE_eval {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) (pt : Fin m → B) :
theorem packedMLE_surjective {m : ℕ} :
theorem packedMLE_unpack {m : ℕ} (t' : MultilinearPoly car.P m) :
theorem packedMLE_val {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :
theorem unpack_coeff {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP) (d : Fin m →₀ ℕ) :
theorem unpack_eval_zeroOne {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP)
theorem unpack_packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :

ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean (7)

example : Function.Injective
example : Function.Injective
example : Function.Injective
example {K L : Type} [Field K] [Field L] [Algebra K L] {ι : Type} [Fintype ι]
theorem openingDecomposition_injective :
theorem recombine_bijective :
theorem recombine_injective :

ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean (22)

def PhasePrvState : Fin (2 + 1) → Type
def honestSlices {m : ℕ} (r : Fin m → car.E) (t' : MultilinearPoly car.P m) :
def pSpecRingSwitchPhase : ProtocolSpec 2
def phaseRBRError : (pSpecRingSwitchPhase car bat).ChallengeIdx → ℝ≥0
def phaseRelIn :
def phaseRelOut :
def phaseWitMid : Fin (2 + 1) → Type
def ringSwitchPhase :
def ringSwitchPhaseProver :
def ringSwitchPhaseRBRKnowledgeSound {σ : Type} (init : ProbComp σ)
def ringSwitchPhaseVerifier :
example (i : (pSpecRingSwitchPhase car bat).ChallengeIdx) (h : i.1 = 1) :
example (r : Fin 3 → decoupledToyCarrier.E)
example :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) :
noncomputable def phaseKnowledgeStateFunction [IsDomain car.E] :
noncomputable def phaseRbrExtractor :
private lemma pr_eq_zero_of_forall_not {α : Type} (D : PMF α) (P : α → Prop)
private theorem phase_badEvent_le
theorem honestSlices_mem_sliceRel {m : ℕ} (r : Fin m → car.E)
theorem ringSwitchPhase_rbrKnowledgeSound [IsDomain car.E] {σ : Type} (init : ProbComp σ)

ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean (22)

def claimConsistent (α : car.ιP → car.E) (s : car.ιE → car.P) : Prop
def evalRel (pc : PackedCommitment P m) :
def openingClaimRel (m : ℕ) :
def sliceRel (m : ℕ) (r : Fin m → car.E) :
def sumcheckClaimRel (m : ℕ) (r : Fin m → car.E) (w : car.ιE → car.P) :
def trivial (P : Type) [CommRing P] (m : ℕ) : PackedCommitment P m where
example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example (r : Fin 3 → decoupledToyCarrier.E) :
example (α : decoupledToyCarrier.ιP → decoupledToyCarrier.E)
example : PackedCommitment decoupledToyCarrier.P 3
example : Type 1
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
theorem aeval_unpack_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem claimConsistent_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem commitsTo_ne_top [Nontrivial P] (pc : PackedCommitment P m) :
theorem commitsTo_not_top [Nontrivial P] (pc : PackedCommitment P m) (c : ∀ j, pc.OStmt j) :
theorem openingClaimRel_of_claimConsistent [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem sumcheckClaim_of_slices {m : ℕ} {r : Fin m → car.E}

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff introduces a large new generic ring-switching layer, fixes a bug in BinaryBasefold, and updates documentation. Overall it follows the ArkLib style guide closely, but a few minor violations were found.

📄 **Per-File Summaries**

ArkLib.lean: Added 9 new imports to ArkLib.lean: ArkLib.Data.Module.Basis, ArkLib.Data.Probability.OracleCompBridge, ArkLib.OracleReduction.Security.ChallengeRound, and six modules under ArkLib.ProofSystem.RingSwitching.Generic (Batching, Carrier, Packing, Recombine, Reduction, Relations). These imports extend the project's support for module bases, a probability oracle compiler bridge, a challenge round in oracle reduction security, and generic ring-switching components in the proof system.
ArkLib/Data/Module/Basis.lean: This new file ArkLib/Data/Module/Basis.lean adds two lemmas to the Module.Basis namespace (for Fintype index types) that characterize the finite R-linear recombination map s ↦ ∑ i, s i • b i associated to a basis b. sum_smul_bijective proves this map is bijective by identifying it with b.equivFun.symm (whose bijectivity follows from equivFun being an isomorphism). sum_smul_injective then derives the corollary that distinct coordinate tuples recombine to distinct module elements. Introducing these lemmas provides a common, reusable reference for both directions of a free-module "pack/unpack" argument, such as those arising in ring-switching proofs.
ArkLib/Data/MvPolynomial/Degrees.lean: Added theorem totalDegree_le_card_of_degreeOf_le_one (in the DegreeOf section) which states that if p : MvPolynomial σ R with Fintype σ satisfies degreeOf i p ≤ 1 for all i, then totalDegree p ≤ Fintype.card σ. This provides a bound on total degree for polynomials that are degree‑at‑most‑1 in each variable, e.g. multilinear polynomials.
ArkLib/Data/MvPolynomial/Multilinear.lean: Added coe_boolFun_eq_ite to relate the Fin 2 → R coercion to an if‑then‑else representation. Added MLE_eval_eq_sum_eqTilde expressing evaluation of the multilinear extension at an arbitrary point as a sum over the hypercube with the eq‑indicator. Added MLE_totalDegree_le bounding the total degree of the multilinear extension by the number of variables. Added aeval_multilinear_eq_sum_eqTilde (with a [IsDomain A] hypothesis) giving an expansion of the aeval of a multilinear polynomial over an R‑algebra in terms of its evaluations on the hypercube.
ArkLib/Data/Probability/Instances.lean: The Schwartz-Zippel lemma prob_schwartz_zippel_mv_polynomial is generalized: its hypothesis now requires a degree bound d : ℕ (renamed from n) and its conclusion gives probability ≤ d / |R| rather than n / |R|. A new lemma prob_schwartz_zippel_single_variable is added: for a non-zero one-variable polynomial f (as an MvPolynomial (Fin 1) R) with total degree ≤ d, the probability it vanishes at a uniformly random point of R is ≤ d / |R|; it is proved by reducing to the multivariate form via prob_uniform_singleton_finFun_eq and Pr_congr.
ArkLib/Data/Probability/OracleCompBridge.lean: This new file ArkLib/Data/Probability/OracleCompBridge.lean introduces two theorems that connect probability statements over VCVio's OracleComp to those over PMF sampling notation, enabling translation between round-by-round security games and per-round error analyses. probEvent_uniformSample_eq_pr_uniformOfFintype equates the event probability of a uniform query $ᵗ C to the PMF-level probability under PMF.uniformOfFintype C. probEvent_bind_uniformSample_le provides a bound for the OracleComp bind of a transcript prefix ma followed by a uniform challenge $ᵗ C, given a per-prefix PMF-level bound, which is the probability core of factoring an RBR (round-by-round) game. The file also establishes the imports VCVio and ArkLib.Data.Probability.Instances with a comment noting the layering precedent.
ArkLib/OracleReduction/Security/ChallengeRound.lean: This new file (ArkLib/OracleReduction/Security/ChallengeRound.lean) introduces two theorems in the Verifier namespace that factor the probability analysis of a single challenge round in round-by-round (RBR) games. probEvent_challengeRound_le proves that if for every fixed prefix outcome a, the PMF-level probability of a bad event q under a uniform challenge is bounded by ε, then the entire game (prefix computation, uniform challenge draw via challengeQueryImpl, and post-processing) also has probability at most ε. probEvent_rbrGame_le is a specialized variant that directly matches the let-bind shape used in Verifier.rbrKnowledgeSoundness (with Prover.runWithLogToRound), providing the same bound without requiring the destructuring bind to be unfolded by whnf. Both theorems are stated over an arbitrary oSpec implementation impl, range over an arbitrary A and β, and use simulateQ with impl.addLift challengeQueryImpl to represent the game's execution.
ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean: Added witnessNovelCoeffs to correctly encode a multilinear witness's Boolean-hypercube table using LSB-first bit ordering (Nat.getBit), replacing the previous inline fun ω => t.val.eval ω which, due to a silent coercion, evaluated at a constant point, making the encoding non‑injective and the consistency predicates vacuously loose. This fix is applied in getMidCodewords and firstOracleWitnessConsistencyProp, both of which now use witnessNovelCoeffs. A regression check (example) verifies that X 0 and X 1 are now distinguished at index 1.
ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: This commit fixes an incorrect call in the sumcheckFoldLens definition inside CoreInteractionPhase.lean. Previously, the lambda fun ω => t.val.eval ω incorrectly used the diagonal evaluations of t; it has been replaced with BinaryBasefold.witnessNovelCoeffs (L := L) t, which correctly reads t's cube table (LSB-first) as required. A comment block explains the reasoning and references a prior fix ("R7 fix"). No sorry or admit were added.
ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: Added the biniusCommitsTo definition, which re-expresses BinaryBasefoldAbstractOStmtIn.initialCompatibility as a commitsTo-oriented predicate for the generic PCS interface, along with the lemma initialCompatibility_eq_biniusCommitsTo proving definitional equality. The docstring notes that the underlying predicate now correctly reads t's cube table via witnessNovelCoeffs (fixing a non-injective encoding issue from the S5 close-review).
ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean: This new file introduces the generic batching separation framework for ring-switching, defining the BatchingStrategy structure (with fields Challenge, weight, error, and a separates theorem) and two proven instances: gammaPowers (γ-power random linear combination, error e/|P|, universal claim count) and eqFold (eq-indicator folding, error κ/|P|, power-of-two claim counts). It provides a reindex method to transport a strategy along a claim-index equivalence, enabling S6 to land instances onto a carrier's opening index. The file also defines decoupledFieldCarrier (P = 𝔽₄, E = 𝔽₈) over ZMod 2 to exercise the [IsDomain P]-gated results, and includes a sanity block with rfl error-bound pins and instantiation examples verifying that the framework applies to concrete fields and the decoupled carrier. No sorry or admit appear.
ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean: This new file introduces RingSwitchCarrier, a structure parameterized by two unrelated B-algebras P and E (each with a B-basis), which serves as the definitional core of the generic ring-switch layer. It defines the packing primitive packedMLE, the eq-decomposition coordinate function eqCoord, the linear bridge map bridge, the auxiliary Bmult multilinear, and proves the key identity bridge_eqTilde linking them via openBasis.repr. Two concrete instances are provided: towerCarrier (where P = E) and decoupledToyCarrier (where P ≠ E over ZMod 2), accompanied by sanity checks that exercise all definitions on both carriers, ensuring the layer does not inadvertently assume P = E.
ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean: This new file introduces the generic packing correctness for ring-switching, proving the semantic content of packing via packedMLE_eval (evaluation at base-embedded points reassembles base evaluations against the packing basis). It also provides the generic unpacking section with unpack, packedMLE_unpack, unpack_packedMLE, packedMLE_surjective, and unpack_eval_zeroOne, establishing a round-trip bijection over any CommRing. Additionally, it proves the Binius-stability bridge packMLE_eq_packedMLE_curry (label 'R2') identifying the DP24 rank-2^κ variable-splitting packMLE with the generic packedMLE applied to the curried family curryFamily.
ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean: This new file adds the generic ring-switching recombination injectivity theorems recombine_bijective, recombine_injective, and openingDecomposition_injective. The first two establish that the packing-basis recombination (step 4, safe-core (iii)) is bijective—hence injective—as required for soundness per Remark 5 of [BRW26], while the third proves injectivity of the opening-basis decomposition, pinning uniqueness of B-coordinates. The file also includes concrete sanity tests exercising these results on both the tower carrier and the decoupled toy carrier, demonstrating that no domain or field hypotheses are needed (pure CommRing + Basis theory).
ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean: This commit introduces ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean, a new file that implements the concrete hand-written ring-switch phase (ProtocolSpec 2) for the generic ring-switching construction. It defines the protocol specification (pSpecRingSwitchPhase), the honest prover's slices (honestSlices) and its prover (ringSwitchPhaseProver), the verifier with a critical claim-consistency check against the input claims (ringSwitchPhaseVerifier), and the combined oracle reduction (ringSwitchPhase). The file establishes the phase's input and output relations (phaseRelIn, phaseRelOut), the round-by-round knowledge error vector (phaseRBRError), and provides the full RBR knowledge-soundness infrastructure: intermediate witness types (phaseWitMid), an extractor (phaseRbrExtractor), a knowledge state function (phaseKnowledgeStateFunction), a bounding lemma for the challenge round's bad event (phase_badEvent_le), and the main theorem ringSwitchPhase_rbrKnowledgeSound (conditioned on [IsDomain car.E]). The module also includes a Sanity section with testable examples instantiating the phase on concrete carriers (tower and decoupled-field) and a pin verifying that the error vector equals the batching strategy's separation error at the challenge round. No sorry or admit is present in this file.
ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean: This new file ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean defines the framework-fixed relation chain (safety pillar 4) and the PCS binding interface (safety pillar 2) for the generic ring-switching layer, adding 450 lines of Lean code. Under RingSwitchCarrier it introduces the anchor relation openingClaimRel (evaluation claims at point r), the intermediate sliceRel (eq-weighted hypercube sums), the batched sumcheckClaimRel, and the chain-coherence theorem sumcheckClaim_of_slices. It also defines the Remark-5 consistency check claimConsistent (comparing claims against slices via both bases), the core theorem aeval_unpack_of_slices (with [IsDomain car.E]), and the completeness/soundness theorems claimConsistent_of_slices and openingClaimRel_of_claimConsistent. The PCS interface is provided by the structure PackedCommitment with the binding predicate commitsTo, its functionality law commitsTo_functional, and the enforcement theorems commitsTo_not_top and commitsTo_ne_top (closing design Hole A). evalRel combines MLPEvalRelation with commitsTo as the anchored input relation. The structure DenseMLPCS extends PackedCommitment with a protocol specification, perfect completeness, and round-by-round knowledge soundness, all stated against the fixed evalRel. A Sanity section includes non-vacuity examples and type‑checking instances on the decoupled and tower carriers, verifying that the relation chain and PCS interface instantiate correctly. The diff contains no sorry or admit.
blueprint/src/references.bib: The blueprint/src/references.bib file is updated to include three new bibliographic entries: BRW26 (Bünz, Rothblum, and Wang's 2026 ePrint paper "Flock: Fast Proving for Batch Boolean Computations"), HJRRR25 (Hemo, Jue, Rabinovich, Roh, and Rothblum's 2025 ePrint paper "Jagged Polynomial Commitments (or: How to Stack Multilinears)"), and RSG (the informal note "Ring switching, generalized" from the leanEthereum/leanVM-b repository, which describes transforming a polynomial commitment scheme for 𝔽₂^f into one for 𝔽₂^e, decoupling packing/opening fields, and γ-power batching). These additions provide the formal citation data for sources that are presumably referenced in the blueprint text.
docs/kb/concepts/ring-switching.md: The documentation file docs/kb/concepts/ring-switching.md was significantly expanded to introduce a new second-generation abstraction called "The Generic layer" (located in ProofSystem/RingSwitching/Generic/), which generalizes from the tower case to decoupled packing and opening algebras P and E (following Flock's Appendix B and the "Ring switching, generalized" note), with tower switching becoming a special case P = E = L.

The addition details the seven-step spine every ring switch shares, the four safety pillars (coordinate maps derived from a bundled Basis, commitment binding through the PCS's own commitsTo, generically proven packing correctness, and no free Prop in the relation chain), and provides a status report for specific files within the Generic layer, each described with its key definitions and proven lemmas.

Newly described files and theorems include:

Carrier.lean: RingSwitchCarrier, bridge_eqTilde (Flock Claim 6's expansion)
Packing.lean: packedMLE_eval, packMLE_eq_packedMLE_curry (the "Binius-stability bridge")
Batching.lean: BatchingStrategy with proven instances gammaPowers and eqFold, plus reindex for transport and the decoupled field carrier label "R5"
Recombine.lean: recombine_bijective / recombine_injective, openingDecomposition_injective (via Module.Basis.sum_smul_bijective)
Relations.lean: The fixed relation chain (openingClaimRel, sliceRel, sumcheckClaimRel), the chain-coherence proof sumcheckClaim_of_slices, plus PCS interface (PackedCommitment, DenseMLPCS) and re-expressed Binius.FRIBinius.biniusCommitsTo

The documentation also notes that Carrier.lean, Packing.lean, Batching.lean, Recombine.lean, and Relations.lean are all proven, sorry-free, and axiom-clean, and clarifies what is not yet built (the assembled ringSwitch reduction, Binius migration, and the MBP-B̂ efficiency layer). Additionally, three new references were added to the Core References section: [BRW26], [RSG], and [HJRRR25].

docs/wiki/repo-map.md: Added documentation for a second-generation ring switching layer under ProofSystem/RingSwitching/Generic/, detailing Carrier.lean (RingSwitchCarrier with decoupled packing/opening algebras), Packing.lean (packing correctness and DP24 bridge), Batching.lean (BatchingStrategy, gammaPowers, eqFold, Schwartz–Zippel under [IsDomain]), Recombine.lean (injectivity on both bases, citing Flock Remark 5 and Data/Module/Basis.lean:sum_smul_bijective), and Relations.lean (relation chain with openingClaimRel, middle relations, PackedCommitment/DenseMLPCS with commitsTo). The new layer is noted as intended to eventually subsume the existing Profile.lean path while leaving it untouched during migration.

Last updated: 2026-07-11 23:48 UTC.

alexanderlhicks · 2026-07-07T15:45:08Z

big next step will be the reduction & soundness.

…rface - Generic/Relations.lean: framework-fixed relation chain — openingClaimRel anchor (+ non-vacuity witness), sliceRel, sumcheckClaimRel, and the proven chain coherence sumcheckClaim_of_slices (via bridge_eqTilde); PackedCommitment (commitsTo + functionality law + Nonempty guard; the legacy True-hook is unstatable: commitsTo_not_top / commitsTo_ne_top); DenseMLPCS mirroring MLIOPCS with relIn fixed to evalRel (= MLPEvalRelation AND commitsTo), so the PCS's own completeness/RBR fields consume the binding predicate - Data/Module/Basis.lean (new): reusable Basis.sum_smul_{bijective,injective}; Recombine.lean refactored onto it + openingDecomposition_injective (the opening half of Flock Remark 5) - Binius/FRIBinius/Prelude.lean: biniusCommitsTo (commitsTo orientation of the legacy initialCompatibility, rfl-pinned); documents the pre-existing upstream diagonal-coercion bug in firstOracleWitnessConsistencyProp (encoding reads t's diagonal evaluations, so commitsTo functionality is unprovable until the upstream spelling is fixed — recorded S7 gate) - KB ring-switching page + repo-map updated; ArkLib.lean regenerated All new declarations sorry-free and axiom-clean; RingSwitching sorry count unchanged at 14; binaryTowerProfile untouched. Hardened via a 4-pass independent adversarial close-review (structural Nonempty guard, precision fixes, upstream bug confirmed by compiled probe and logged). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

firstOracleWitnessConsistencyProp, getMidCodewords, and the honest-witness lens in FRIBinius/CoreInteractionPhase built P0 from `fun w => t.val.eval w`, where the silent coercion Fin (2^l) -> (Fin l -> L) is the pointwise Nat-cast CONSTANT function — the "novel coefficients" were t's evaluations at diagonal points, not its hypercube table, making the encoding non-injective (X 0 and X 1 collapsed definitionally; compiled counterexample) and the predicate unusable as binding semantics (functionality provably false). Fix: new named encoder BinaryBasefold.witnessNovelCoeffs — t's cube table in the LSB-first Nat.getBit order, the exact inverse of the decoder's Nat.binaryFinMapToNat mapping (roundtrip: getBit_of_binaryFinMapToNat) — used at all three sites; a repo-wide sweep found no further instances. Compiled regression probe: witnessNovelCoeffs now separates X 0 / X 1. The biniusCommitsTo functionality proof (S7) is provable-as-sketched again. Pre-existing bug (predates this PR); all consumers are sorry-gated statements, so nothing proven was invalidated. Found by the S5 close-review adversarial passes. Docstrings and the KB page updated accordingly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Review finding: the R7 regression probe was verified in-session but never committed, so nothing in-tree would catch the diagonal-encoding bug regressing. Adds a generic-field example separating witnessNovelCoeffs (X 0) from (X 1) at omega = 1 - unprovable under the pre-fix diagonal spelling. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Two plumbing lemmas for RBR-game factoring (generic ring-switch S6): - probEvent_uniformSample_eq_pr_uniformOfFintype: Pr[E | $t C] equals the PMF-level Pr_{c <-$p C}[E c] - probEvent_bind_uniformSample_le: a per-prefix PMF bound transfers to the bind (prefix; uniform challenge; pair) - the challenge-round shape Both sorry-free and axiom-clean ([propext, Classical.choice, Quot.sound]). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Verifier.probEvent_challengeRound_le: bounds the RBR-game shape (prefix; uniformly sampled challenge i; post-map) by any epsilon that bounds the PMF-level bad-event probability for every fixed prefix outcome - the bridge from simulateQ (impl.addLift challengeQueryImpl) games to Pr_{c <- $p _} per-round analyses (BatchingStrategy.separates). The prefix is an arbitrary OracleComp (no prover unfolding); the post-map covers the games' (transcript, challenge, queryLog) triple. Sorry-free, axiom-clean. Closes the bootstrapped 'medium' plumbing item; the feared erw-chain reduced to one erw [simulateQ_query]. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

… check (S6/F2) The design-review F2 algebra, all sorry-free and axiom-clean: - Packing.lean: generic unpack (coefficient-wise packBasis.repr) with the round-trip PROVEN both directions (packedMLE_unpack / unpack_packedMLE; packedMLE_surjective constructive) - CommRing-only, honoring the file's no-assumed-round-trip disclaimer - Relations.lean: claimConsistent (DP24 Check 1 in family form, the [BRW26] Remark-5 read-back equation) + both directions: openingClaimRel_of_claimConsistent (soundness read-back, [IsDomain E] - the logged S6 deviation) and claimConsistent_of_slices (completeness) - Data/MvPolynomial/Multilinear.lean: aeval_multilinear_eq_sum_eqTilde (eq-expansion of a multilinear at an algebra point; reusable) INV-2: exercised on tower, decoupled-toy (CommRing-only parts) and decoupled-field (domain-gated parts) carriers. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…uction Generic/Reduction.lean: the ProtocolSpec 2 phase (prover sends slices, verifier sends batching challenge) written WITHOUT the composition operators, so every definition is sorry-free and axiom-clean (verified: standard 3 axioms on all 8 public decls) despite upstream OracleVerifier.append.verify being sorried. - Verifier performs the soundness-critical claim-consistency check (design review F1: without it the phase RBR statement is false), and fails via OptionT failure, not a dummy statement - phaseRelIn = openingClaimRel AND commitsTo (packedMLE wit) - the oracle-extended anchor promised at S5; phaseRelOut carries commitsTo through to the sumcheck claim - Per-round error VECTOR (bat.error at the single challenge round) - WitMid/extractor via unpack; RBR knowledge soundness recorded as a Prop-valued def (roadmap section 8, F3) pending the stretch proof - W := car.iE pinned; INV-2 examples on tower + decoupled-field carriers Also folds ChallengeRound.lean + Reduction.lean into the ArkLib.lean umbrella (283 imports). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…o first) ringSwitchPhase_rbrKnowledgeSound: the ring-switch phase is round-by-round knowledge sound with error bat.error at the batching-challenge round - the FIRST non-vacuous RBR probability bound completed in ArkLib (the three prior real ones are all sorried). - phaseKnowledgeStateFunction [IsDomain car.E]: round 1 tracks the Remark-5 check + binding + slice relation; round 2 re-tracks the check (the verifier fails without it), binding, and the batched claim; toFun_full cases on the verifier's definitional if and kills the failure branch by empty support - phase_badEvent_le: commitsTo_functional collapses the existential to the committed t'0; the surviving event is exactly BatchingStrategy.separates on the sent slices vs the honest slices of t'0 (via sumcheckClaim_of_slices); no-commitment branch has probability zero - Verifier.probEvent_rbrGame_le (Security/ChallengeRound.lean): the factoring lemma restated at the literal game shape - unifying the game's destructuring bind against the plain-bind lemma diverges in whnf (structure-eta through the prover term), so the same proof script is replayed with the matcher fired by one constructor-level obtain All axiom-clean ([propext, Classical.choice, Quot.sound]); zero sorry tokens; no maxHeartbeats override needed; whole library green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Independent adversarial close-review verdict: theorem holds up, 'repo first' claim accurate, no blockers. Adds its two suggested witnesses: phaseRelIn nonemptiness (true claims + trivial commitment - the RBR obligation is not discharged by an empty input relation) and an end-to-end application of ringSwitchPhase_rbrKnowledgeSound at decoupledFieldCarrier with the PROVEN gamma-powers strategy (real separation error 3/4). Honest caveats recorded in roadmap section 8: phase completeness deferred (next session), and the repo-wide RBR->knowledge-soundness implication remains sorried upstream. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ter hardening (checkpoint) WIP checkpoint (one temporary sorry in Generic/Reduction.lean — the verifier-side support peel of ringSwitchPhase_perfectCompleteness). NOT for push; C-SORRY-in-Generic is momentarily 1 by design of this checkpoint. Everything else builds green and is sorry-free. Landed this session: - Ported the OptionT support-peel toolkit from feat/abf26-plan (same VCVio pin, strict supersets): ToVCVio/.../SimulateQ.lean (OptionT run-bind/lift peelers, probEvent_eq_one_of_simulateQ_support_bind) and OracleReduction/Execution.lean (per-direction processRound unfolds). - PCS B-2 honest-committer hardening (Relations.lean): PackedCommitment now carries `commit` + `commitsTo_commit` (subsumes the bare `neC` nonemptiness guard); new commitsTo_ne_bot (False-hook unstatable, dual to commitsTo_ne_top) and evalRel_nonempty (PCS input relation provably nonempty — S5 close-review residual B-2 closed). - Phase completeness (Reduction.lean): point-form honest_mem_phaseRelOut and honest_claimConsistent PROVEN; the protocol-level ringSwitchPhase_perfectCompleteness has its full prover-run peel + verifier-query resolution working, one sorry at the final support read-off (resume notes inline). Also validated (not in this commit, scratch): F4 relation-chain gate probe compiles — commitsTo threads phaseRelIn -> phaseRelOut -> sumcheck rounds -> pcs.evalRel -> acceptRejectOracleRel end to end. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…er query resolution Extends the f0c1d70 checkpoint. ringSwitchPhase_perfectCompleteness now has the full prover-run peel (challenge fixed), the verifier slice-query resolution (`hq`), and the Remark-5 check discharge (`hcheck`) all compiling; the lone remaining sorry is the final verifier-side support read-off — a pure monadic-normalization step (OptionT.pure-bind is defeq but not syntactic). Resume notes inline point to porting the toy protocol's `verifierBody_simulateQ_eq_pure` pattern as a dedicated value lemma. Builds green; RingSwitching/Generic sorry = 1 (this WIP), non-generic still 14; Data/Fin/* pre-existing sorries untouched. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

…s (S6 phase completeness DONE) The final verifier-side support read-off is closed by re-ascribing `hx` to its defeq-collapsed forms (`replace hx : … := hx`, accepted by isDefEq) — bridging the OptionT.pure-bind gap that blocks syntactic `pure_bind`/`if_pos` — then `if_pos hcheck` and a final defeq collapse to `pure (some finalValue)`; closes with `honest_mem_phaseRelOut` (relOut) and `rfl` (prover/verifier statement agreement). `classical` threads the verifier's `Classical.propDecidable` instance. Independently verified: `lake build …Generic.Reduction` green (3596 jobs); `#print axioms ringSwitchPhase_perfectCompleteness` = [propext, Classical.choice, Quot.sound] (no sorryAx); source scan clean. RingSwitching/Generic now sorry-free again; non-generic C-SORRY still 14. The phase security package (RBR knowledge soundness + perfect completeness) is now fully certified — closes the S5/S6 close-review "half-certified" concern. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

… (INV-2, non-domain P) Bundles Hachi's proven `psi_bijective` ([NOZ26] §3 Theorem 2) into a `Basis` and instantiates `RingSwitchCarrier` with `B = E = R_q^H` (the fixed subfield) and `P = R_q`. Why it matters: * INV-2 in its strongest form to date. The two existing carriers (`towerCarrier`, `decoupledFieldCarrier`) are both field packing algebras; this one has a NON-DOMAIN `P`. Four `example`s apply the generic results (`recombine_bijective`, `openingDecomposition_injective`, `bridge_eqTilde`, `packedMLE_eval`) to it verbatim — none needs `[IsDomain P]`, which is exactly the honest fork working as designed. * The generic carrier now covers all four established packing-family ring switches: DP24/Binius, the [RSG] decoupled note, Flock App. B, and Hachi §3. * `ιE = Unit`: Hachi's subfield-valued evaluation point makes the opening basis a singleton, which is the structural reason [NOZ26] §3's relocation is deterministic where DP24's is interactive. Data layer only — the reduction-level collapse is not claimed here. Also adds the missing `Nontrivial (Rq (powTwoCyclotomic α))` instance (belongs upstream in `CyclotomicRing/`, kept local for now). Sorry-free; all declarations axiom-clean ([propext, Classical.choice, Quot.sound]). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…undary Adds the `HachiCarrier.lean` status entry, an explicit coverage statement (the generic carrier instantiates at all four established packing-family switches: DP24/Binius, RSG, Flock App. B, Hachi §3), and the honest-fork upgrade from asserted to demonstrated. Also states the boundary plainly: the HMZ25 `Lift` switch is NOT covered — its transport map is not a ring map, so the packing-`Basis` vocabulary does not reach it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

github-actions · 2026-08-02T00:29:12Z

🤖 PR Summary

The PR introduces a new generic ring-switching framework that generalizes the previous tower-specific RingSwitchingProfile to a decoupled packing/opening algebra over an arbitrary base ring. The core is a new RingSwitchCarrier structure parameterized by two B-algebras P (packing) and E (opening), each with a B-basis, plus nontriviality and finiteness. On this carrier, the framework defines packedMLE (packing a family of multilinears), eqCoord (coordinate of the eq indicator), bridge (the unique linear map from E to P), and Bmult (the auxiliary multiplier). The key identity bridge_eqTilde is proved. A BatchingStrategy structure with two proven instances (gammaPowers and eqFold) provides the Schwartz–Zippel–based separation guarantees needed for the round‑by‑round proof. The Recombine file proves bijectivity and injectivity of the recombination and opening decomposition maps, establishing the safe‑core properties (design step 4). The Relations file defines the fixed relation chain (openingClaimRel, sliceRel, sumcheckClaimRel) and the PackedCommitment interface with commitsTo, DenseMLPCS, and the claimConsistent check; it proves chain coherence and the completeness/soundness directions of claimConsistent. The Reduction file defines the full hand‑written ring‑switch phase as an OracleReduction and proves its round‑by‑round knowledge soundness (S6 stretch goal) and perfect completeness. The HachiCarrier file instantiates the carrier for Hachi’s §3 packing head with a non‑domain P = R_q and confirms the generic theorems apply. Supporting changes include: new theorems in MvPolynomial (multilinear expansions, degree bounds), a refactored Schwartz–Zippel lemma (explicit degree parameter, single‑variable variant), a new ChallengeRound security theorem bridging OracleComp to PMF‑level bounds, and a bug fix in Binius where witnessNovelCoeffs now correctly reads the multilinear’s hypercube table (LSB‑first) instead of the non‑injective diagonal evaluation. The ArkLib import hub is updated to expose the new modules. Documentation (docs/kb/concepts/ring-switching.md and docs/wiki/repo-map.md) is updated to describe the new generic layer, and three new references are added to blueprint/src/references.bib. No sorry or admit placeholders are introduced anywhere in the diff.

Statistics

Metric	Count
📝 Files Changed	22
✅ Lines Added	3240
❌ Lines Removed	12

Lean Declarations

✏️ Added: 150 declaration(s)

ArkLib/Data/Module/Basis.lean (2)

theorem sum_smul_bijective (b : Basis ι R M) :
theorem sum_smul_injective (b : Basis ι R M) :

ArkLib/Data/MvPolynomial/Degrees.lean (1)

theorem totalDegree_le_card_of_degreeOf_le_one [Fintype σ] (p : MvPolynomial σ R)

ArkLib/Data/MvPolynomial/Multilinear.lean (4)

theorem MLE_eval_eq_sum_eqTilde (evals : (σ → Fin 2) → R) (r : σ → R) :
theorem MLE_totalDegree_le (evals : (σ → Fin 2) → R) :
theorem aeval_multilinear_eq_sum_eqTilde {A : Type*} [CommRing A] [Algebra R A] [IsDomain A]
theorem coe_boolFun_eq_ite [AddMonoidWithOne R] (u : σ → Fin 2) :

ArkLib/Data/Probability/Instances.lean (1)

lemma prob_schwartz_zippel_single_variable {R : Type} [CommRing R] [IsDomain R] [Fintype R]

ArkLib/Data/Probability/OracleCompBridge.lean (2)

theorem probEvent_bind_uniformSample_le {A : Type} (ma : ProbComp A)
theorem probEvent_uniformSample_eq_pr_uniformOfFintype (E : C → Prop) :

ArkLib/OracleReduction/Execution.lean (3)

theorem Prover.processRound_of_dir_eq_P_to_V (j : Fin n) (hDir : pSpec.dir j = .P_to_V)
theorem Prover.processRound_of_dir_eq_V_to_P (j : Fin n) (hDir : pSpec.dir j = .V_to_P)
theorem Prover.runToRound_succ (i : Fin n)

ArkLib/OracleReduction/Security/ChallengeRound.lean (2)

theorem probEvent_challengeRound_le
theorem probEvent_rbrGame_le

ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean (2)

def witnessNovelCoeffs (t : L⦃≤ 1⦄[X Fin ℓ]) : Fin (2^ℓ) → L
example :

ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean (2)

def biniusCommitsTo
lemma initialCompatibility_eq_biniusCommitsTo :

ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean (14)

def decoupledFieldCarrier : RingSwitchCarrier (ZMod 2) where
def eqFold (κ : ℕ) : BatchingStrategy P (Fin κ → Fin 2) where
def gammaPowers (e : ℕ) : BatchingStrategy P (Fin e) where
def reindex {P : Type} [CommRing P] {W : Type} [Fintype W] (bat : BatchingStrategy P W)
example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (e : ℕ) :
example (P : Type) [CommRing P] [IsDomain P] [Fintype P] (κ : ℕ) :
example : BatchingStrategy (ZMod 3) (Fin (2 ^ 2))
example : BatchingStrategy (ZMod 3) (Fin 3)
example : Type 1
example : decoupledFieldCarrier.P = GaloisField 2 2
example :
example :
example :
example :

ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean (15)

def Bmult {m : ℕ} (r : Fin m → car.E) (weight : car.ιE → car.P) : MultilinearPoly car.P m
def boolToE {m : ℕ} (y : Fin m → Fin 2) : Fin m → car.E
def bridge (weight : car.ιE → car.P) : car.E →ₗ[B] car.P
def decoupledToyCarrier : RingSwitchCarrier (ZMod 2) where
def eqCoord {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2) (u : car.ιE) : B
def packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) : MultilinearPoly car.P m
def towerCarrier {K L : Type} [Field K] [Field L] [Algebra K L]
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2) (u : decoupledToyCarrier.ιE) :
example (r : Fin 3 → decoupledToyCarrier.E) (y : Fin 3 → Fin 2)
example (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example : RingSwitchCarrier (ZMod 2)
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
theorem bridge_eqTilde {m : ℕ} (r : Fin m → car.E) (y : Fin m → Fin 2)

ArkLib/ProofSystem/RingSwitching/Generic/HachiCarrier.lean (9)

def hachiPackBasis (α κ : ℕ) (h2 : (2 : ZMod q) ≠ 0) (hk : 2 * 2 ^ κ ∣ 2 ^ α) :
def hachiPackingCarrier (α κ : ℕ) (h2 : (2 : ZMod q) ≠ 0) (hk : 2 * 2 ^ κ ∣ 2 ^ α) :
def psiEquiv (α κ : ℕ) (h2 : (2 : ZMod q) ≠ 0) (hk : 2 * 2 ^ κ ∣ 2 ^ α) :
def psiLin (α κ : ℕ) :
example : Function.Bijective
example : Function.Injective
example {m : ℕ} (Ps : (hachiPackingCarrier q α κ h2 hk).ιP →
example {m : ℕ} (r : Fin m → (hachiPackingCarrier q α κ h2 hk).E) (y : Fin m → Fin 2)
instance instNontrivialRqPowTwo (α : ℕ) :

ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean (14)

def curryFamily {κ ℓ ℓ' : ℕ} {K : Type} [CommRing K] (h_l : ℓ = ℓ' + κ)
def unpack {m : ℕ} (t' : MultilinearPoly car.P m) : car.ιP → MultilinearPoly B m
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) (pt : Fin 3 → ZMod 2) :
example (Ps : decoupledToyCarrier.ιP → MultilinearPoly (ZMod 2) 3) :
example (t' : MultilinearPoly decoupledToyCarrier.P 3) :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) (m : ℕ) :
theorem packMLE_eq_packedMLE_curry {κ : ℕ} [NeZero κ] {K L : Type} [Field K] [Field L] [Algebra K L]
theorem packedMLE_eval {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) (pt : Fin m → B) :
theorem packedMLE_surjective {m : ℕ} :
theorem packedMLE_unpack {m : ℕ} (t' : MultilinearPoly car.P m) :
theorem packedMLE_val {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :
theorem unpack_coeff {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP) (d : Fin m →₀ ℕ) :
theorem unpack_eval_zeroOne {m : ℕ} (t' : MultilinearPoly car.P m) (i : car.ιP)
theorem unpack_packedMLE {m : ℕ} (Ps : car.ιP → MultilinearPoly B m) :

ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean (7)

example : Function.Injective
example : Function.Injective
example : Function.Injective
example {K L : Type} [Field K] [Field L] [Algebra K L] {ι : Type} [Fintype ι]
theorem openingDecomposition_injective :
theorem recombine_bijective :
theorem recombine_injective :

ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean (25)

def PhasePrvState : Fin (2 + 1) → Type
def honestSlices {m : ℕ} (r : Fin m → car.E) (t' : MultilinearPoly car.P m) :
def pSpecRingSwitchPhase : ProtocolSpec 2
def phaseRBRError : (pSpecRingSwitchPhase car bat).ChallengeIdx → ℝ≥0
def phaseRelIn :
def phaseRelOut :
def phaseWitMid : Fin (2 + 1) → Type
def ringSwitchPhase :
def ringSwitchPhaseProver :
def ringSwitchPhaseRBRKnowledgeSound {σ : Type} (init : ProbComp σ)
def ringSwitchPhaseVerifier :
example (i : (pSpecRingSwitchPhase car bat).ChallengeIdx) (h : i.1 = 1) :
example (r : Fin 3 → decoupledToyCarrier.E)
example :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {σ : Type} (init : ProbComp σ) (impl : QueryImpl []ₒ (StateT σ ProbComp)) :
noncomputable def phaseKnowledgeStateFunction [IsDomain car.E] :
noncomputable def phaseRbrExtractor :
private lemma pr_eq_zero_of_forall_not {α : Type} (D : PMF α) (P : α → Prop)
private theorem phase_badEvent_le
theorem honestSlices_mem_sliceRel {m : ℕ} (r : Fin m → car.E)
theorem honest_claimConsistent [IsDomain car.E]
theorem honest_mem_phaseRelOut
theorem ringSwitchPhase_perfectCompleteness [IsDomain car.E] :
theorem ringSwitchPhase_rbrKnowledgeSound [IsDomain car.E] {σ : Type} (init : ProbComp σ)

ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean (24)

def claimConsistent (α : car.ιP → car.E) (s : car.ιE → car.P) : Prop
def evalRel (pc : PackedCommitment P m) :
def openingClaimRel (m : ℕ) :
def sliceRel (m : ℕ) (r : Fin m → car.E) :
def sumcheckClaimRel (m : ℕ) (r : Fin m → car.E) (w : car.ιE → car.P) :
def trivial (P : Type) [CommRing P] (m : ℕ) : PackedCommitment P m where
example (r : Fin 3 → decoupledToyCarrier.E) (w : decoupledToyCarrier.ιE → decoupledToyCarrier.P) :
example (r : Fin 3 → decoupledToyCarrier.E) :
example (α : decoupledToyCarrier.ιP → decoupledToyCarrier.E)
example : PackedCommitment decoupledToyCarrier.P 3
example : Type 1
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L) :
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {K L ι : Type} [Field K] [Field L] [Algebra K L] [Fintype ι] (β : Basis ι K L)
example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
example {m : ℕ} {r : Fin m → decoupledFieldCarrier.E}
theorem aeval_unpack_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem claimConsistent_of_slices [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem commitsTo_ne_bot (pc : PackedCommitment P m) :
theorem commitsTo_ne_top [Nontrivial P] (pc : PackedCommitment P m) :
theorem commitsTo_not_top [Nontrivial P] (pc : PackedCommitment P m) (c : ∀ j, pc.OStmt j) :
theorem evalRel_nonempty (pc : PackedCommitment P m) : pc.evalRel.Nonempty
theorem openingClaimRel_of_claimConsistent [IsDomain car.E] {m : ℕ} {r : Fin m → car.E}
theorem sumcheckClaim_of_slices {m : ℕ} {r : Fin m → car.E}

ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean (23)

@[simp] lemma mapQuery_mk {α} (impl : QueryImpl spec m)
lemma OptionT.failure_bind.{u, v} {m : Type u → Type v} [Monad m] [LawfulMonad m]
lemma OptionT.probEvent_eq_one_of_simulateQ_support_bind
lemma OracleComp.eq_of_mem_support_pure
lemma OracleComp.mem_support_bind_peel
lemma OracleComp.mem_support_map_peel
lemma liftM_eq_liftComp_liftM {κ : Type} {spec₃ : OracleSpec κ}
lemma mem_support_run_bind
lemma mem_support_run_lift_bind
lemma simulateQ_addLift_add_liftM_left
lemma simulateQ_addLift_add_liftM_right
lemma simulateQ_add_add_liftM_comp_base (t : spec.Domain) :
lemma simulateQ_add_add_liftM_comp_left (t : spec₁.Domain) :
lemma simulateQ_add_add_liftM_comp_right (t : spec₂.Domain) :
lemma simulateQ_add_add_liftM_query_base (t : spec.Domain) :
lemma simulateQ_add_add_liftM_query_left (t : spec₁.Domain) :
lemma simulateQ_add_add_liftM_query_right (t : spec₂.Domain) :
lemma simulateQ_liftM_query [LawfulMonad r] {ι' : Type} {spec' : OracleSpec ι'} {α : Type}
lemma simulateQ_optionT_failure
lemma simulateQ_optionT_forIn_yield_pure_none
lemma simulateQ_optionT_forIn_yield_pure_some
lemma simulateQ_optionT_liftM_run_eq_of_query
lemma simulateQ_optionT_list_forIn

sorry Tracking

No sorrys were added, removed, or affected.

📄 **Per-File Summaries**

ArkLib.lean: The diff adds nine new import lines to ArkLib.lean, which serves as the top-level import hub for the library. Three new imports are in the Data namespace: ArkLib.Data.Module.Basis and ArkLib.Data.Probability.OracleCompBridge. One new import is in OracleReduction.Security: ArkLib.OracleReduction.Security.ChallengeRound. The remaining six imports are under ArkLib.ProofSystem.RingSwitching.Generic: Batching, Carrier, HachiCarrier, Packing, Recombine, Reduction, and Relations. These additions make the corresponding modules available project-wide, reflecting the introduction of new formalizations for module bases, probability oracle compilation, challenge-round security, and generic ring-switching infrastructure.
ArkLib/Data/Module/Basis.lean: This new file adds two theorems, sum_smul_bijective and sum_smul_injective, to the Module.Basis namespace. sum_smul_bijective proves that the map s ↦ ∑ i, s i • b i (s : ι → R, b : Basis ι R M) is bijective by identifying it with b.equivFun.symm and appealing to the bijectivity of equivFun. sum_smul_injective deduces injectivity directly from the bijectivity lemma.
ArkLib/Data/MvPolynomial/Degrees.lean: Added theorem totalDegree_le_card_of_degreeOf_le_one in MvPolynomial/Degrees.lean, which states that for a polynomial p over a finite variable type σ, if each p.degreeOf i ≤ 1 then p.totalDegree ≤ Fintype.card σ. The proof expands totalDegree via Finset.sup_le, rewrites the sum of exponents with Finsupp.sum_fintype, and uses the hypothesis to bound each m i by 1, yielding the cardinality bound.
ArkLib/Data/MvPolynomial/Multilinear.lean: Added three new theorems and one new lemma to ArkLib/Data/MvPolynomial/Multilinear.lean. coe_boolFun_eq_ite proves the Boolean-point coercion (u : σ → R) equals the if-then-else expression fun i => if u i = 1 then 1 else 0. MLE_eval_eq_sum_eqTilde gives an expansion formula: MvPolynomial.eval r (MLE evals) = ∑ x : σ → Fin 2, eqTilde (x : σ → R) r * evals x. MLE_totalDegree_le establishes an upper bound on total degree: (MLE evals).totalDegree ≤ Fintype.card σ. aeval_multilinear_eq_sum_eqTilde states that for a multilinear polynomial p over R, evaluating at r in an R-algebra A expands as aeval r p = ∑ y : σ → Fin 2, eqTilde (y : σ → A) r * algebraMap R A (eval (y : σ → R) p), subject to the hypothesis that A is a domain (noted as future work to relax). No sorry or admit were added in the diff.
ArkLib/Data/Probability/Instances.lean: The multivariate Schwartz-Zippel lemma prob_schwartz_zippel_mv_polynomial was refactored: its degree bound is now an explicit parameter d : ℕ instead of reusing the number of variables n, and its docstring now says 'finite integral domain' instead of 'finite field'. A new lemma prob_schwartz_zippel_single_variable was added, providing the same bound for a single-variable polynomial evaluated at a uniformly random element of R, by reducing to the multivariate case via prob_uniform_singleton_finFun_eq.
ArkLib/Data/Probability/OracleCompBridge.lean: This file introduces a bridge between VCVio's OracleComp event probability notation (Pr[E | oa]) and the PMF-level sampling notation (Pr_{ let c ← $ᵖ C}[E c]) used for round-by-round security proofs. It provides two theorems: probEvent_uniformSample_eq_pr_uniformOfFintype, which equates the probability of an event under a uniform oracle query $ᵗ C with its probability under PMF.uniformOfFintype C; and probEvent_bind_uniformSample_le, which lifts a per-prefix PMF-level bound on E a c to a bound on the OracleComp bind do let a ← ma; let c ← $ᵗ C; return (a, c) — the shape of the final challenge round in an RBR game. No sorry or admit are present.
ArkLib/OracleReduction/Execution.lean: The commit adds four new theorems to ArkLib/OracleReduction/Execution.lean:

Prover.runToRound_succ expresses running a prover up to round i.succ as running up to round i.castSucc then processing round i, providing a general successor-step alternative to Fin.induction for unfolding multi-round runs.
Prover.processRound_of_dir_eq_V_to_P resolves the processRound body for challenge rounds (pSpec.dir j = .V_to_P), showing it reads the prior result, draws the challenge via pSpec.getChallenge, feeds it to prover.receiveChallenge, and appends the challenge to the transcript.
Prover.processRound_of_dir_eq_P_to_V analogously resolves processRound for message rounds (pSpec.dir j = .P_to_V), showing it reads the prior result, runs prover.sendMessage, and appends the resulting message to the transcript.

ArkLib/OracleReduction/Security/ChallengeRound.lean: Added ChallengeRound.lean with two theorems probEvent_challengeRound_le and probEvent_rbrGame_le in the Verifier namespace. probEvent_challengeRound_le factors the probability of a bad event after a prefix computation and a uniform challenge into the per‑prefix uniform‑challenge probability bound, bridging the round‑by‑round game to the PMF‑level analyses used by per‑round error lemmas. probEvent_rbrGame_le is a game‑shaped variant that directly applies to the Verifier.rbrKnowledgeSoundness structure, avoiding whnf divergence by destructing the prover term at the constructor level.
ArkLib/ProofSystem/Binius/BinaryBasefold/Basic.lean: The diff redefines witnessNovelCoeffs — previously inlined as fun ω => t.val.eval ω, whose silent coercion made it read the diagonal evaluations of t (all coordinates set to the same value ω) — to correctly encode the multilinear witness as its Boolean-hypercube table using LSB-first bit order via Nat.getBit. A regression test example proves that under the new encoding the monomials X 0 and X 1 yield distinct coefficient vectors at ω = 1. Both getMidCodewords and firstOracleWitnessConsistencyProp are updated to call the new witnessNovelCoeffs instead of the old fun ω => t.val.eval ω, thereby fixing the consistency predicates so they compare the genuine hypercube evaluation against the oracle instead of the (non-injective) diagonal evaluation. No sorry or admit are introduced.
ArkLib/ProofSystem/Binius/FRIBinius/CoreInteractionPhase.lean: In sumcheckFoldCtxLens, the computation of P₀ is changed from polynomialFromNovelCoeffsF₂ K β ℓ' (by omega) (fun ω => t.val.eval ω) to polynomialFromNovelCoeffsF₂ K β ℓ' (by omega) (BinaryBasefold.witnessNovelCoeffs (L := L) t). The previous inline lambda silently read t's diagonal evaluations (a bug), while the new call uses BinaryBasefold.witnessNovelCoeffs to correctly obtain t's cube table (LSB-first), fixing the coefficient extraction.
ArkLib/ProofSystem/Binius/FRIBinius/Prelude.lean: This PR adds a new definition biniusCommitsTo, a re-oriented version of the oracle-consistency predicate (matching RingSwitching.Generic.PackedCommitment.commitsTo's signature), which states that the initial oracle commits to a multilinear t iff firstOracleWitnessConsistencyProp t f₀ holds for the first oracle. It also proves initialCompatibility_eq_biniusCommitsTo — a rfl lemma establishing that this new predicate is definitionally identical to the legacy BinaryBasefoldAbstractOStmtIn.initialCompatibility, clarifying it's a semantic no-op (the S5 re-orientation). The docstrings record that the underlying predicate reads t's cube table via witnessNovelCoeffs (LSB-first bit order) rather than the original non-injective diagonal reading, and that the S7 obligation is the functionality proof commitsTo c t → commitsTo c t' → t = t', provable by unique decoding. No sorry or admit is added.
ArkLib/ProofSystem/RingSwitching/Generic/Batching.lean: This new file (290 lines) introduces the BatchingStrategy structure and its two proven instances for design step 5 of the generic ring switch. BatchingStrategy is defined with fields Challenge, weight, error, and separates (a Schwartz–Zippel guarantee) and is gated only on [CommRing P], with domain/finiteness hypotheses reserved for the instances. The file provides gammaPowers (γ-power random linear combination, universal claim count e, error e/|P|) and eqFold (eq-indicator folding for Boolean cube {0,1}^κ, error κ/|P|), both with completed separates proofs reducing to the generic prob_schwartz_zippel_mv_polynomial. A reindex function transports a strategy along an equivalence of claim-index types. The file also defines decoupledFieldCarrier (a RingSwitchCarrier with P = 𝔽₄, E = 𝔽₈) and includes sanity examples pinning errors, instantiating strategies over concrete fields (e.g., GaloisField 2 4, ZMod 3, ZMod 6) and exercising the decoupled carrier with [IsDomain P] gating to satisfy gate R5. No sorries or admits are present.
ArkLib/ProofSystem/RingSwitching/Generic/Carrier.lean: This file introduces the generic ring-switching carrier RingSwitchCarrier as a structure parameterized by a base ring B, containing two unrelated B-algebras P (packing) and E (opening), each with a B-basis (packBasis, openBasis), along with nontriviality and finiteness assumptions. It defines derived operations: boolToE (embedding boolean hypercube points into E), packedMLE (packing a family of B-valued multilinears into a single P-valued multilinear via packBasis), eqCoord (the u-th B-coordinate of eq(r,y) in the opening basis), bridge (the unique B-linear map from E to P determined by a weight function), and Bmult (the auxiliary multiplier Φ(eq(r,y)) as a P-multilinear). The theorem bridge_eqTilde establishes the key identity that bridge applied to eq(r,y) equals the weighted sum of eqCoord. Two concrete instances are provided: towerCarrier (the DP24/Binius special case where P = E = L with a single basis) and decoupledToyCarrier (a minimal witness with P ≠ E of distinct ranks over ZMod 2, ensuring no definition assumes P = E). The file ends with sanity-check examples verifying that both carriers build and that the derived definitions and bridge_eqTilde apply on the decoupled carrier. No sorry or admit are present.
ArkLib/ProofSystem/RingSwitching/Generic/HachiCarrier.lean: Adds the file ArkLib/ProofSystem/RingSwitching/Generic/HachiCarrier.lean, which instantiates a RingSwitchCarrier for Hachi's §3 packing head. It defines instNontrivialRqPowTwo (nontriviality of the cyclotomic ring), psiLin (the linear packing map), psiEquiv (the linear equivalence of Theorem 2 in [NOZ26]), hachiPackBasis (a Basis derived from that equivalence), and hachiPackingCarrier (the carrier with P = R_q – a non‑domain – and E the fixed subfield). Four example blocks then apply the generic RingSwitchCarrier theorems (recombine_bijective, openingDecomposition_injective, bridge_eqTilde, packedMLE_eval) to this carrier, confirming that each holds without a [IsDomain P] hypothesis.
ArkLib/ProofSystem/RingSwitching/Generic/Packing.lean: This new file provides the generic packing correctness theorem packedMLE_eval for RingSwitchCarrier, expressing the evaluation of the packed multilinear at a base-ring point as the sum of base evaluations against the packing basis. It introduces unpack as a section of packedMLE and proves the round-trip lemmas packedMLE_unpack, unpack_packedMLE, and packedMLE_surjective, all over any CommRing. It defines curryFamily and proves packMLE_eq_packedMLE_curry, the "Binius-stability bridge" identifying DP24's packMLE variable-splitting with the generic packedMLE applied to the curried family over the tower carrier. The file also includes sanity-check examples instantiating these results on the decoupled carrier, demonstrating that the generic proofs are CommRing-only and hold for P != E cases.
ArkLib/ProofSystem/RingSwitching/Generic/Recombine.lean: This new file in the Generic ring-switching module adds three theorems and five sanity-check examples. The theorem recombine_bijective proves that the map sending a B-coordinate tuple to the packed sum ∑ i, s i • car.packBasis i is bijective, using the packBasis basis property. recombine_injective derives the injectivity of that recombination map (design step 4, corresponding to safe-core (iii) and BRW26 Remark 5), and openingDecomposition_injective proves the analogous injectivity for the opening basis car.openBasis to pin unique B-coordinate decompositions. The file also provides five concrete sanity-check example blocks exercising these theorems on specific carriers: the tower carrier for a general finite-rank field extension, the tower carrier with the concrete Basis.singleton over ZMod 2, and the decoupled P ≠ E carrier (again over ZMod 2), verifying both packing and opening injectivity without domain/field hypotheses. No sorry or admit are present.
ArkLib/ProofSystem/RingSwitching/Generic/Reduction.lean: This new file (Reduction.lean) defines the hand-written ring-switch phase of the generic ring-switching pipeline, as an OracleReduction without composition operators (sorry‑free and axiom‑clean). It introduces pSpecRingSwitchPhase (protocol spec with two rounds), the honest prover ringSwitchPhaseProver, the verifier ringSwitchPhaseVerifier (which enforces the central claimConsistent check), the combined ringSwitchPhase, the input/output relations phaseRelIn/phaseRelOut, the round‑by‑round error vector phaseRBRError, the intermediate‑witness types phaseWitMid, the extractor phaseRbrExtractor, and the knowledge‑state function phaseKnowledgeStateFunction. The file then proves ringSwitchPhase_rbrKnowledgeSound (the S6 stretch‑goal theorem, using phase_badEvent_le and the batching strategy’s separates property) and ringSwitchPhase_perfectCompleteness, together with auxiliary completeness lemmas honest_mem_phaseRelOut and honest_claimConsistent. Sanity examples demonstrate instantiation on concrete carriers and commitments.
ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean: This new file (ArkLib/ProofSystem/RingSwitching/Generic/Relations.lean) defines the framework-fixed relation chain for the generic ring-switching layer: openingClaimRel (the input anchor), sliceRel (eq‑weighted hypercube sums of the packed polynomial), and sumcheckClaimRel (the batched sumcheck input). It proves chain coherence via sumcheckClaim_of_slices and formalises the Remark‑5 consistency check (claimConsistent) with its completeness direction (claimConsistent_of_slices) and soundness read‑back to the anchor (openingClaimRel_of_claimConsistent), both relying on the core identity aeval_unpack_of_slices (which requires [IsDomain car.E]). For the PCS binding interface, it introduces the PackedCommitment structure with the binding predicate commitsTo, the functionality law commitsTo_functional, and the honest committer commit (plus its correctness commitsTo_commit); it then proves that the trivial hook fun _ _ => True and the empty hook fun _ _ => False are impossible (commitsTo_not_top, commitsTo_ne_top, commitsTo_ne_bot). Finally, it defines evalRel (the anchored input relation combining evaluation correctness with commitsTo) and the DenseMLPCS structure extending PackedCommitment with perfect completeness and RBR knowledge soundness stated against that fixed relation. The file also includes sanity examples verifying that the relations typecheck on the decoupled and tower carriers, that claimConsistent is statable without domain hypotheses, and that the soundness/completeness theorems instantiate on the decoupled field carrier where [IsDomain E] holds.
ArkLib/ToVCVio/OracleComp/SimSemantics/SimulateQ.lean: Added an import of VCVio.OracleComp.SimSemantics.OptionT.Basic and then introduced 17 new lemmas and one simp lemma. These include OptionT.probEvent_eq_one_of_simulateQ_support_bind (a bind-prefixed variant for initial state from ProbComp), support-peeling lemmas (mem_support_run_bind, mem_support_run_lift_bind, OracleComp.mem_support_bind_peel, OracleComp.eq_of_mem_support_pure, OracleComp.mem_support_map_peel), a mapQuery_mk simplifier, simulateQ_liftM_query for lifted queries, simulateQ_optionT_list_forIn for OptionT-monadic forIn, six routing lemmas for the spec + (spec₁ + spec₂) sum layout (simulateQ_add_add_liftM_query_* and simulateQ_add_add_liftM_comp_*), simulateQ_addLift_add_liftM_left/right for three-way addLift resolution, and OptionT.failure_bind, simulateQ_optionT_failure, simulateQ_optionT_forIn_yield_pure_some, simulateQ_optionT_forIn_yield_pure_none dealing with OptionT failure and guarded forIn loops. Many of these are marked as staged for upstream VCV-io.
blueprint/src/references.bib: Added three new BibTeX entries to the references file: Bünz, Rothblum, and Wang's 'Flock: Fast Proving for Batch Boolean Computations' (ePrint 2026/1329); Hemo, Jue, Rabinovich, Roh, and Rothblum's 'Jagged Polynomial Commitments (or: How to Stack Multilinears)' (ePrint 2025/917); and an internal note 'Ring switching, generalized' from the leanEthereum/leanVM-b repository, which explains how to transform a polynomial commitment scheme for F_{2^f} into one for F_{2^e} for arbitrary e and f, with decoupled packing/opening fields and gamma-power batching. These references likely support new cryptographic constructions or results used in the project.
docs/kb/concepts/ring-switching.md: documentation for docs/kb/concepts/ring-switching.md was updated to describe a new second-generation abstraction layer in ProofSystem/RingSwitching/Generic/, which generalizes from the previous tower-specific RingSwitchingProfile to a decoupled packing/opening algebra framework. The update catalogs the newly introduced structures and proven theorems (RingSwitchCarrier, packedMLE/eqCoord/bridge/Bmult, bridge_eqTilde, packedMLE_eval, packMLE_eq_packedMLE_curry, BatchingStrategy with instances gammaPowers and eqFold, recombine_bijective/recombine_injective/openingDecomposition_injective, the relation chain openingClaimRel/sliceRel/sumcheckClaimRel and sumcheckClaim_of_slices, PackedCommitment with commitsTo, DenseMLPCS), the hachiPackingCarrier for a non-domain P (with psi_bijective/psiLin/psiEquiv, and four example applications of generic results), and the coverage status of four packing-family ring switches (DP24/Binius, decoupled, Hachi) and what is excluded (HMZ25 Lift). It also notes what is not yet built: the assembled ringSwitch reduction, the Binius migration, and the MBP efficiency layer, and adds new core references. The diff contains no sorry or admit.
docs/wiki/repo-map.md: The documentation in docs/wiki/repo-map.md now describes a new second-generation ring-switching layer under ProofSystem/RingSwitching/Generic/, listing its components: Carrier.lean (RingSwitchCarrier with decoupled packing/opening algebras), Packing.lean (packing correctness + DP24 bridge), Batching.lean (batching strategies, gammaPowers, eqFold, and Schwartz–Zippel under [IsDomain]), Recombine.lean (injectivity via sum_smul_bijective, referencing Flock Remark 5), and Relations.lean (openingClaimRel, middle relations, PackedCommitment/DenseMLPCS with commitsTo). It notes that this layer is intended to eventually subsume the existing Profile.lean path, which remains untouched during migration.

Last updated: 2026-08-02 00:29 UTC.

start generalizing

af91401

alexanderlhicks changed the title ~~start generalizing~~ feat: even more general ring switch Jul 7, 2026

alexanderlhicks and others added 13 commits July 7, 2026 23:54

style(Data/MvPolynomial): show -> change (Data zero-warning budget)

86f9f0f

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

This was referenced Jul 24, 2026

feat/refactor(Hachi): ring switching subprotocol #654

Merged

feat(Hachi): formalize lemma 10 of the paper #656

Open

refactor(Hachi/CWSS): cwss packages with escape #659

Open

alexanderlhicks and others added 2 commits August 2, 2026 01:04

alexanderlhicks mentioned this pull request Aug 2, 2026

feat: completeness and rbrKnowledgeSoundness of FRI-Binius protocols #383

Open

Navigation Menu

Uh oh!

feat: even more general ring switch - #615

feat: even more general ring switch#615
alexanderlhicks wants to merge 16 commits into
mainfrom
feat/generic-ring-switch

alexanderlhicks commented Jul 7, 2026

Uh oh!

github-actions Bot commented Jul 7, 2026 •

edited

Loading

Uh oh!

alexanderlhicks commented Jul 7, 2026

Uh oh!

github-actions Bot commented Aug 2, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

alexanderlhicks commented Jul 7, 2026

Uh oh!

github-actions Bot commented Jul 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

alexanderlhicks commented Jul 7, 2026

Uh oh!

github-actions Bot commented Aug 2, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Jul 7, 2026 •

edited

Loading

github-actions Bot commented Aug 2, 2026 •

edited

Loading